(set-logic QF_AUFNIA)
(set-info :status sat)
(declare-fun |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| () Int)
(declare-fun |ssl3_accept_#t~mem38_491| () Int)
(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state| () Int)
(declare-fun ssl3_accept_~s.offset_12 () Int)
(declare-fun ssl3_accept_~s.base_12 () Int)
(declare-fun |#memory_int_136| () (Array Int (Array Int Int)))
(declare-fun |ssl3_accept_#t~mem35_173| () Int)
(declare-fun |ssl3_accept_#t~mem49_513| () Int)
(declare-fun |ssl3_accept_#t~mem29_161| () Int)
(declare-fun |#memory_int_53| () (Array Int (Array Int Int)))
(declare-fun |ssl3_accept_#t~mem24_68| () Int)
(declare-fun |#memory_int_601| () (Array Int (Array Int Int)))
(declare-fun |ssl3_accept_#t~mem31_631| () Int)
(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num| () Int)
(declare-fun |#memory_$Pointer$.base_53| () (Array Int (Array Int Int)))
(declare-fun |#memory_$Pointer$.base_52| () (Array Int (Array Int Int)))
(declare-fun |ssl3_accept_#t~nondet159_515| () Int)
(declare-fun ssl3_accept_~ret~10_753 () Int)
(declare-fun ssl3_accept_~ret~10_314 () Int)
(declare-fun |ssl3_accept_#t~mem22_459| () Int)
(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3| () Int)
(declare-fun |#memory_$Pointer$.offset_521| () (Array Int (Array Int Int)))
(declare-fun |ssl3_accept_#t~mem165.offset_593| () Int)
(declare-fun |ssl3_accept_#t~mem23_461| () Int)
(declare-fun |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| () Int)
(assert
 (let (($x220 (= |#offset~STRUCT#?type~INT?length~UINT?off~UINT?data~$Pointer$?input~$Pointer$?comp~$Pointer$#~data| 12)))
 (let (($x2621 (= |ssl3_accept_#t~mem38_491| 8544)))
 (let (($x2622 (not $x2621)))
 (let (($x10875 (not $x2622)))
 (let (($x23085 (and $x10875 $x220)))
 (not $x23085)))))))
(assert
 (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
 (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12)))
 (let ((?x1400 (select ?x1399 ?x806)))
 (let (($x1478 (>= |ssl3_accept_#t~mem35_173| ?x1400)))
 (not $x1478))))))
(assert
 (let (($x2678 (>= |ssl3_accept_#t~mem49_513| 8640)))
 (not $x2678)))
(assert
 (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
 (let ((?x1399 (select |#memory_int_136| ssl3_accept_~s.base_12)))
 (let ((?x1400 (select ?x1399 ?x806)))
 (let (($x1447 (<= |ssl3_accept_#t~mem29_161| ?x1400)))
 (let ((?x1089 (select |#memory_int_53| ssl3_accept_~s.base_12)))
 (let ((?x1090 (select ?x1089 ?x806)))
 (let (($x1113 (>= |ssl3_accept_#t~mem24_68| ?x1090)))
 (let (($x19982 (and $x1113 $x1447)))
 (not $x19982))))))))))
(assert
 (let ((?x806 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~state|)))
 (let ((?x3029 (select |#memory_int_601| ssl3_accept_~s.base_12)))
 (let ((?x3030 (select ?x3029 ?x806)))
 (let (($x3088 (>= |ssl3_accept_#t~mem31_631| ?x3030)))
 (let ((?x1050 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~init_num|)))
 (let ((?x1051 (select |#memory_$Pointer$.base_53| ssl3_accept_~s.base_12)))
 (let ((?x1032 (select |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12)))
 (let ((?x1054 (store |#memory_$Pointer$.base_52| ssl3_accept_~s.base_12 (store ?x1032 ?x1050 (select ?x1051 ?x1050)))))
 (let (($x1055 (= |#memory_$Pointer$.base_53| ?x1054)))
 (let (($x11490 (and $x1055 $x3088)))
 (not $x11490))))))))))))
(assert
 (let (($x3458 (>= ssl3_accept_~ret~10_753 |ssl3_accept_#t~nondet159_515|)))
 (let (($x2065 (not (<= ssl3_accept_~ret~10_314 0))))
 (let (($x50182 (and $x2065 $x3458)))
 (not $x50182)))))
(assert
 (let (($x2542 (not (= |ssl3_accept_#t~mem22_459| 16384))))
 (let ((?x1068 (+ ssl3_accept_~s.offset_12 |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~s3|)))
 (let ((?x2719 (select |#memory_$Pointer$.offset_521| ssl3_accept_~s.base_12)))
 (let ((?x2734 (select ?x2719 ?x1068)))
 (let (($x2925 (<= |ssl3_accept_#t~mem165.offset_593| ?x2734)))
 (and $x2925 $x2542)))))))
(assert
 (let (($x2547 (not (= |ssl3_accept_#t~mem23_461| 8192))))
 (let (($x73 (= |#offset~STRUCT#?version~INT?type~INT?method~$Pointer$?rbio~$Pointer$?wbio~$Pointer$?bbio~$Pointer$?rwstate~INT?in_handshake~INT?handshake_func~$Pointer$?server~INT?new_session~INT?quiet_shutdown~INT?shutdown~INT?state~INT?rstate~INT?init_buf~$Pointer$?init_num~INT?init_off~INT?packet~$Pointer$?packet_length~UINT?s2~$Pointer$?s3~$Pointer$?read_ahead~INT?hit~INT?purpose~INT?trust~INT?cipher_list~$Pointer$?cipher_list_by_id~$Pointer$?enc_read_ctx~$Pointer$?read_hash~$Pointer$?expand~$Pointer$?enc_write_ctx~$Pointer$?write_hash~$Pointer$?compress~$Pointer$?cert~$Pointer$?sid_ctx_length~UINT?sid_ctx~ARRAY#_32_~UCHAR#?session~$Pointer$?verify_mode~INT?verify_depth~INT?verify_callback~$Pointer$?info_callback~$Pointer$?error~INT?error_code~INT?ctx~$Pointer$?debug~INT?verify_result~LONG?ex_data~~CRYPTO_EX_DATA?client_CA~$Pointer$?references~INT?options~ULONG?mode~ULONG?first_packet~INT?client_version~INT#~packet| 72)))
 (let (($x11452 (and $x73 $x2547)))
 (not $x11452)))))
(check-sat)
